Proof verification in GEB

% Remco Bloemen % 2010-01-03, last updated 2014-03-04

In Hofstadter's book Gödel, Escher, Bach he discusses a few formal systems. In this post I have translated the two simplest of them to my simple proof verification system which, as suggested by Sander’s comment, is extended with a command to define a constant.

The MIU-System

C M
C I
C U

T 'Sole axiom'
        ⊨ M I
∎

T 'Rule I'
        ∧ x I
        ⊨ x I U
∎

T 'Rule II'
        ∧ M x
        ⊨ M x x
∎

T 'Rule III'
        ∧ x I I I y
        ⊨ x U y
∎

T 'Rule IV'
        ∧ x U U y
        ⊨ x y
∎

With the system defined, I can now enter the derivation of MUIIU:

T 'Derivation of M U I I U'
        ∵ 'Sole axiom'
        ∵ 'Rule II'
                x ⊧ I
        ∵ 'Rule II'
                x ⊧ I I
        ∵ 'Rule II'
                x ⊧ I I
        ∵ 'Rule I'
                x ⊧ M I I I I
        ∵ 'Rule III'
                x ⊧ M
                y ⊧ I U
        ∵ 'Rule III'
                x ⊧ M
                y ⊧ I U
        ∵ 'Rule II'
                x ⊧ U I U
        ∵ 'Rule IV'
                x ⊧ M U I
                y ⊧ I U
        ∴ M U I I U
∎

The pq-System

The pq-system is not that formal in the book, it contains expressions such as "whenever x is composed of hyphens only" that are not further specified. Luckily, it is easy to formalise these statements in my proof language:

C p
C q
C -
C ComposedOfHyphens

T 'ComposedOfHyphens -'
        ⊨ ComposedOfHyphens -
∎

T 'ComposedOfHyphens a b'
        ∧ ComposedOfHyphens a
        ∧ ComposedOfHyphens b
        ⊨ ComposedOfHyphens a b
∎

T 'The Axiom'
        ∧ ComposedOfHyphens x
        ⊨ x p - q x -
∎

T 'The Rule'
        ∧ ComposedOfHyphens x
        ∧ ComposedOfHyphens y
        ∧ ComposedOfHyphens z
        ∧ x p y q z
        ⊨ x p y - z -
∎